Papers with automated theorem proving
Logical Inferences with Comparatives and Generalized Quantifiers (2020.acl-srw)
Copied to clipboard
| Challenge: | Comparative constructions pose a challenge in Natural Language Inference (NLI) Comparatives interact with quantifiers, numerals, and lexical antonyms, but a logical inference system for comparatives has not been developed for the task. |
| Approach: | They propose a compositional semantics system that maps comparative constructions to semantic representations via combinatory categorial grammar parsers and integrates it with an automated theorem proving system. |
| Outcome: | The proposed system outperforms previous logic-based systems and deep learning models on three NLI datasets. |
CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization (2026.acl-long)
Copied to clipboard
Zhongyuan Peng, Yifan Yao, Kaijing Ma, Shuyue Guo, Yizhe Li, Yichi Zhang, Chenchen Zhang, Yifan Zhang, Zhouliang Yu, Luming Li, Minghao Liu, Yihang Xia, Jiawei Shen, Yuchen Wu, Yixin Cao, Zhaoxiang Zhang, Wenhao Huang, Jiaheng Liu, Ge Zhang
| Challenge: | Existing approaches to formalizing mathematical statements face limitations in accuracy, especially in the context of complex, highlevel problems that involve sophisticated mathematical reasoning. |
| Approach: | They propose a CriticLean framework that elevates the role of the critic from a passive validator to an active learning component and introduce a benchmark to measure models’ ability to distinguish semantically correct from incorrect formalizations. |
| Outcome: | The proposed framework outperforms open- and closed-source benchmarks and shows that it significantly outperformed existing models. |